A, C, B:Type, eqa:EqDecider(A), eqc, eqc':EqDecider(C), r:(AC), f:a:A fp B, a:A, z:B, c:C.
Inj(A; C; r)  c = r(a)  rename(r;f)(c)?z = f(a)?z  B 

latex

Definitions	P  Q, Inj(A; B; f), a:A fp B(a), EqDecider(T), Prop, x. t(x), x:A. B(x), f(x)?z, rename(r;f), t  T
Lemmas	fpf-cap wf, deq wf, fpf wf, inject wf, fpf-rename-cap2, fpf-rename wf